(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
group3(@l) → group3#1(@l)
group3#1(::(@x, @xs)) → group3#2(@xs, @x)
group3#1(nil) → nil
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y)
group3#2(nil, @x) → nil
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs))
group3#3(nil, @x, @y) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys)
zip3#2(nil, @l3, @x, @xs) → nil
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
zip3#3(nil, @x, @xs, @y, @ys) → nil
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6, 7, 8]
transitions:
::0(0, 0) → 0
nil0() → 0
tuple#30(0, 0, 0) → 0
group30(0) → 1
group3#10(0) → 2
group3#20(0, 0) → 3
group3#30(0, 0, 0) → 4
zip30(0, 0, 0) → 5
zip3#10(0, 0, 0) → 6
zip3#20(0, 0, 0, 0) → 7
zip3#30(0, 0, 0, 0, 0) → 8
group3#11(0) → 1
group3#21(0, 0) → 2
nil1() → 2
group3#31(0, 0, 0) → 3
nil1() → 3
tuple#31(0, 0, 0) → 9
group31(0) → 10
::1(9, 10) → 4
nil1() → 4
zip3#11(0, 0, 0) → 5
zip3#21(0, 0, 0, 0) → 6
nil1() → 6
zip3#31(0, 0, 0, 0, 0) → 7
nil1() → 7
zip31(0, 0, 0) → 11
::1(9, 11) → 8
nil1() → 8
group3#12(0) → 10
group3#21(0, 0) → 1
nil1() → 1
group3#31(0, 0, 0) → 2
::1(9, 10) → 3
zip3#12(0, 0, 0) → 11
zip3#21(0, 0, 0, 0) → 5
nil1() → 5
zip3#31(0, 0, 0, 0, 0) → 6
::1(9, 11) → 7
group3#31(0, 0, 0) → 1
::1(9, 10) → 2
zip3#31(0, 0, 0, 0, 0) → 5
::1(9, 11) → 6
group3#21(0, 0) → 10
nil1() → 10
zip3#21(0, 0, 0, 0) → 11
nil1() → 11
group3#31(0, 0, 0) → 10
::1(9, 10) → 1
zip3#31(0, 0, 0, 0, 0) → 11
::1(9, 11) → 5
::1(9, 10) → 10
::1(9, 11) → 11
(2) BOUNDS(1, n^1)